Nuprl Definition : one_one_corr
13,42
postcript
pdf
1-1-Corresp(
A
;
B
) ==
f
:
A
B
.
g
:
B
A
. InvFuns(
A
;
B
;
f
;
g
)
latex
Up
fun
1
,
fun
1
Wellformedness Lemmas
one
one
corr
wf
,
one
one
corr
wf
Definitions
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
InvFuns(
A
;
B
;
f
;
g
)
FDL editor aliases
one_one_corr
origin
f:A
B. g:BA. InvFuns(A;B;f;g) f:AB. g:BA. InvFuns(A;B;f;g) x:A. B(x)B(x)